<!DOCTYPE html>
<html class="writer-html5" lang="en" >
<head>
    <meta charset="utf-8" />
    <meta http-equiv="X-UA-Compatible" content="IE=edge" />
    <meta name="viewport" content="width=device-width, initial-scale=1.0" />
      <link rel="shortcut icon" href="../../img/favicon.ico" />
    <title>命题逻辑 - 咩咩的笔记</title>
    <link rel="stylesheet" href="../../css/theme.css" />
    <link rel="stylesheet" href="../../css/theme_extra.css" />
        <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/10.5.0/styles/github.min.css" />
    
      <script>
        // Current page data
        var mkdocs_page_name = "\u547d\u9898\u903b\u8f91";
        var mkdocs_page_input_path = "\u79bb\u6563\u6570\u5b66\\2-\u547d\u9898\u903b\u8f91.md";
        var mkdocs_page_url = null;
      </script>
    
    <script src="../../js/jquery-3.6.0.min.js" defer></script>
    <!--[if lt IE 9]>
      <script src="../../js/html5shiv.min.js"></script>
    <![endif]-->
      <script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/10.5.0/highlight.min.js"></script>
      <script>hljs.initHighlightingOnLoad();</script> 
</head>

<body class="wy-body-for-nav" role="document">

  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side stickynav">
    <div class="wy-side-scroll">
      <div class="wy-side-nav-search">
          <a href="../.." class="icon icon-home"> 咩咩的笔记
        </a><div role="search">
  <form id ="rtd-search-form" class="wy-form" action="../../search.html" method="get">
      <input type="text" name="q" placeholder="Search docs" aria-label="Search docs" title="Type search term here" />
  </form>
</div>
      </div>

      <div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul>
                <li class="toctree-l1"><a class="reference internal" href="../..">主页</a>
                </li>
              </ul>
              <p class="caption"><span class="caption-text">笔记</span></p>
              <ul class="current">
                  <li class="toctree-l1"><a class="reference internal" href="#">线性代数</a>
    <ul>
                <li class="toctree-l2"><a class="reference internal" href="../../%E7%BA%BF%E6%80%A7%E4%BB%A3%E6%95%B0/0-%E5%89%8D%E8%A8%80/">0-前言</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E7%BA%BF%E6%80%A7%E4%BB%A3%E6%95%B0/1-%E7%BA%BF%E6%80%A7%E6%96%B9%E7%A8%8B%E7%BB%84/">1-线性方程组</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E7%BA%BF%E6%80%A7%E4%BB%A3%E6%95%B0/2-%E7%9F%A9%E9%98%B5%E4%BB%A3%E6%95%B0/">2-矩阵代数</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E7%BA%BF%E6%80%A7%E4%BB%A3%E6%95%B0/3-%E8%A1%8C%E5%88%97%E5%BC%8F/">3-行列式</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E7%BA%BF%E6%80%A7%E4%BB%A3%E6%95%B0/4-%E5%90%91%E9%87%8F%E7%A9%BA%E9%97%B4/">4-向量空间</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E7%BA%BF%E6%80%A7%E4%BB%A3%E6%95%B0/5-%E7%89%B9%E5%BE%81%E5%80%BC%E4%B8%8E%E7%89%B9%E5%BE%81%E5%90%91%E9%87%8F/">5-特征值与特征向量</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E7%BA%BF%E6%80%A7%E4%BB%A3%E6%95%B0/6-%E6%AD%A3%E4%BA%A4%E6%80%A7%E4%B8%8E%E6%9C%80%E5%B0%8F%E4%BA%8C%E4%B9%98/">6-正交性与最小二乘</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E7%BA%BF%E6%80%A7%E4%BB%A3%E6%95%B0/7-%E5%AF%B9%E7%A7%B0%E9%98%B5%E4%B8%8E%E4%BA%8C%E6%AC%A1%E5%9E%8B/">7-对称阵与二次型</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E7%BA%BF%E6%80%A7%E4%BB%A3%E6%95%B0/8-%E5%90%91%E9%87%8F%E7%A9%BA%E9%97%B4%E7%9A%84%E5%87%A0%E4%BD%95/">8-向量空间的几何</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E7%BA%BF%E6%80%A7%E4%BB%A3%E6%95%B0/%E9%99%84%E5%BD%95A-3Blue1Brown%E7%AC%94%E8%AE%B0/">附录A-3Blue1Brown笔记</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E7%BA%BF%E6%80%A7%E4%BB%A3%E6%95%B0/%E9%99%84%E5%BD%95B-%E9%9B%B6%E7%A9%BA%E9%97%B4%E4%B8%8E%E5%88%97%E7%A9%BA%E9%97%B4%E7%9A%84%E5%AF%B9%E6%AF%94/">附录B-零空间与列空间的对比</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E7%BA%BF%E6%80%A7%E4%BB%A3%E6%95%B0/%E9%99%84%E5%BD%95C-%E9%80%86%E7%9F%A9%E9%98%B5%E5%AE%9A%E7%90%86/">附录C-逆矩阵定理</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E7%BA%BF%E6%80%A7%E4%BB%A3%E6%95%B0/%E9%99%84%E5%BD%95D-%E6%80%9D%E7%BB%B4%E5%AF%BC%E5%9B%BE/">附录D-思维导图</a>
                </li>
    </ul>
                  </li>
                  <li class="toctree-l1"><a class="reference internal" href="#">数字电路</a>
    <ul>
                <li class="toctree-l2"><a class="reference internal" href="../../%E6%95%B0%E5%AD%97%E7%94%B5%E8%B7%AF/1.%20%E4%BB%8B%E7%BB%8D/">介绍</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E6%95%B0%E5%AD%97%E7%94%B5%E8%B7%AF/2.%20%E6%95%B0%E5%AD%97%E7%B3%BB%E7%BB%9F%E3%80%81%E8%BF%90%E7%AE%97%E5%92%8C%E7%BC%96%E7%A0%81/">数字系统、运算和编码</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E6%95%B0%E5%AD%97%E7%94%B5%E8%B7%AF/3.%20%E9%80%BB%E8%BE%91%E9%97%A8/">逻辑门</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E6%95%B0%E5%AD%97%E7%94%B5%E8%B7%AF/4.%20%E5%B8%83%E5%B0%94%E4%BB%A3%E6%95%B0/">布尔代数</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E6%95%B0%E5%AD%97%E7%94%B5%E8%B7%AF/5.%20%E7%BB%84%E5%90%88%E9%80%BB%E8%BE%91%E5%88%86%E6%9E%90/">组合逻辑分析</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E6%95%B0%E5%AD%97%E7%94%B5%E8%B7%AF/6.%20%E7%BB%84%E5%90%88%E9%80%BB%E8%BE%91%E5%8A%9F%E8%83%BD%E6%A8%A1%E5%9D%97/">组合逻辑功能模块</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E6%95%B0%E5%AD%97%E7%94%B5%E8%B7%AF/7.%20%E9%94%81%E5%AD%98%E5%99%A8%E3%80%81%E8%A7%A6%E5%8F%91%E5%99%A8%E5%92%8C%E5%AE%9A%E6%97%B6%E5%99%A8/">锁存器、触发器和定时器</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E6%95%B0%E5%AD%97%E7%94%B5%E8%B7%AF/8.%20%E7%A7%BB%E4%BD%8D%E5%AF%84%E5%AD%98%E5%99%A8/">移位寄存器</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E6%95%B0%E5%AD%97%E7%94%B5%E8%B7%AF/9.%20%E8%AE%A1%E6%95%B0%E5%99%A8/">计数器</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E6%95%B0%E5%AD%97%E7%94%B5%E8%B7%AF/10.%20%E5%82%A8%E5%AD%98%E5%99%A8/">储存器</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E6%95%B0%E5%AD%97%E7%94%B5%E8%B7%AF/11.%20%E6%A8%A1%E6%95%B0%E8%BD%AC%E6%8D%A2/">模数转换</a>
                </li>
    </ul>
                  </li>
                  <li class="toctree-l1 current"><a class="reference internal current" href="#">离散数学</a>
    <ul class="current">
                <li class="toctree-l2 current"><a class="reference internal current" href="./">命题逻辑</a>
    <ul class="current">
    <li class="toctree-l3"><a class="reference internal" href="#_2">基本概念</a>
    </li>
    <li class="toctree-l3"><a class="reference internal" href="#_3">语法</a>
    </li>
    <li class="toctree-l3"><a class="reference internal" href="#_4">语义</a>
    </li>
    <li class="toctree-l3"><a class="reference internal" href="#_5">等值演算</a>
    </li>
    <li class="toctree-l3"><a class="reference internal" href="#_6">范式</a>
    </li>
    <li class="toctree-l3"><a class="reference internal" href="#_7">推理理论</a>
        <ul>
    <li class="toctree-l4"><a class="reference internal" href="#_8">派生规则</a>
    </li>
        </ul>
    </li>
    <li class="toctree-l3"><a class="reference internal" href="#_9">应用</a>
        <ul>
    <li class="toctree-l4"><a class="reference internal" href="#_10">自然语言命题的符号化</a>
    </li>
    <li class="toctree-l4"><a class="reference internal" href="#_11">普通逻辑问题的符号化</a>
    </li>
    <li class="toctree-l4"><a class="reference internal" href="#_12">算法性质的逻辑分析</a>
    </li>
        </ul>
    </li>
    </ul>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../3-%E4%B8%80%E9%98%B6%E9%80%BB%E8%BE%91/">一阶逻辑</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../4-%E8%AF%81%E6%98%8E%E6%96%B9%E6%B3%95/">证明方法</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../5-%E9%9B%86%E5%90%88/">集合</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../6-%E5%85%B3%E7%B3%BB/">关系</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../7-%E5%87%BD%E6%95%B0/">函数</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../8-%E8%AE%A1%E6%95%B0%E4%B8%8E%E7%BB%84%E5%90%88/">计数与组合</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../9-%E5%9B%BE%E4%B8%8E%E6%A0%91/">图与树</a>
                </li>
    </ul>
                  </li>
                  <li class="toctree-l1"><a class="reference internal" href="#">计算机组成原理</a>
    <ul>
                <li class="toctree-l2"><a class="reference internal" href="../../%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BB%84%E6%88%90%E5%8E%9F%E7%90%86/1.%20%E8%AE%A1%E7%AE%97%E6%9C%BA%E6%A6%82%E8%A7%88/">计算机概览</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BB%84%E6%88%90%E5%8E%9F%E7%90%86/2.%20%E6%8C%87%E4%BB%A4/">指令</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BB%84%E6%88%90%E5%8E%9F%E7%90%86/3.%20%E8%AE%A1%E7%AE%97%E6%9C%BA%E4%B8%AD%E7%9A%84%E8%BF%90%E7%AE%97/">计算机中的运算</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BB%84%E6%88%90%E5%8E%9F%E7%90%86/4.%20MIPS%20CPU%E8%AE%BE%E8%AE%A1/">MIPS CPU设计</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BB%84%E6%88%90%E5%8E%9F%E7%90%86/5.%20%E5%AD%98%E5%82%A8%E5%99%A8%E5%B1%82%E6%AC%A1%E7%BB%93%E6%9E%84/">存储器层次结构</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BB%84%E6%88%90%E5%8E%9F%E7%90%86/6.%20%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%B3%BB%E7%BB%9F%E6%80%BB%E7%BA%BF/">计算机系统总线</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BB%84%E6%88%90%E5%8E%9F%E7%90%86/7.%20%E8%BE%93%E5%85%A5%E8%BE%93%E5%87%BA%E7%B3%BB%E7%BB%9F/">输入输出系统</a>
                </li>
    </ul>
                  </li>
                  <li class="toctree-l1"><a class="reference internal" href="#">计算机组成原理实验</a>
    <ul>
                <li class="toctree-l2"><a class="reference internal" href="../../%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BB%84%E6%88%90%E5%8E%9F%E7%90%86%E5%AE%9E%E9%AA%8C/1/1/">加法器</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BB%84%E6%88%90%E5%8E%9F%E7%90%86%E5%AE%9E%E9%AA%8C/2/2/">有限状态机</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BB%84%E6%88%90%E5%8E%9F%E7%90%86%E5%AE%9E%E9%AA%8C/3/3/">MIPS指令集1</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BB%84%E6%88%90%E5%8E%9F%E7%90%86%E5%AE%9E%E9%AA%8C/4/4/">MIPS指令集2</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BB%84%E6%88%90%E5%8E%9F%E7%90%86%E5%AE%9E%E9%AA%8C/5/5/">存储器实验</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BB%84%E6%88%90%E5%8E%9F%E7%90%86%E5%AE%9E%E9%AA%8C/6/6/">寄存器堆与 ALU 设计实验</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BB%84%E6%88%90%E5%8E%9F%E7%90%86%E5%AE%9E%E9%AA%8C/7/7/">存储器与控制器实验</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BB%84%E6%88%90%E5%8E%9F%E7%90%86%E5%AE%9E%E9%AA%8C/8/8/">单周期处理器实验</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BB%84%E6%88%90%E5%8E%9F%E7%90%86%E5%AE%9E%E9%AA%8C/9/9/">多周期处理器实验</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E8%AE%A1%E7%AE%97%E6%9C%BA%E7%BB%84%E6%88%90%E5%8E%9F%E7%90%86%E5%AE%9E%E9%AA%8C/10/10/">多周期处理器综合性开放实验</a>
                </li>
    </ul>
                  </li>
                  <li class="toctree-l1"><a class="reference internal" href="#">概率论</a>
    <ul>
                <li class="toctree-l2"><a class="reference internal" href="../../%E6%A6%82%E7%8E%87%E8%AE%BA/1.%20%E6%A6%82%E7%8E%87%E8%AE%BA%E7%9A%84%E5%9F%BA%E6%9C%AC%E6%A6%82%E5%BF%B5/">概率论的基本概念</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E6%A6%82%E7%8E%87%E8%AE%BA/2.%20%E9%9A%8F%E6%9C%BA%E5%8F%98%E9%87%8F%E5%8F%8A%E5%85%B6%E5%88%86%E5%B8%83/">随机变量及其分布</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E6%A6%82%E7%8E%87%E8%AE%BA/3.%20%E5%A4%9A%E7%BB%B4%E9%9A%8F%E6%9C%BA%E5%8F%98%E9%87%8F%E5%8F%8A%E5%85%B6%E5%88%86%E5%B8%83/">多维随机变量及其分布</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E6%A6%82%E7%8E%87%E8%AE%BA/4.%20%E9%9A%8F%E6%9C%BA%E5%8F%98%E9%87%8F%E7%9A%84%E6%95%B0%E5%AD%97%E7%89%B9%E5%BE%81/">随机变量的数字特征</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E6%A6%82%E7%8E%87%E8%AE%BA/5.%20%E5%A4%A7%E6%95%B0%E5%AE%9A%E5%BE%8B%E5%8F%8A%E4%B8%AD%E5%BF%83%E6%9E%81%E9%99%90%E5%AE%9A%E7%90%86/">大数定律及中心极限定理</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E6%A6%82%E7%8E%87%E8%AE%BA/6.%20%E6%A0%B7%E6%9C%AC%E5%8F%8A%E6%8A%BD%E6%A0%B7%E5%88%86%E5%B8%83/">样本及抽样分布</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E6%A6%82%E7%8E%87%E8%AE%BA/7.%20%E5%8F%82%E6%95%B0%E4%BC%B0%E8%AE%A1/">参数估计</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E6%A6%82%E7%8E%87%E8%AE%BA/8.%20%E5%81%87%E8%AE%BE%E9%AA%8C%E8%AF%81/">假设验证</a>
                </li>
    </ul>
                  </li>
                  <li class="toctree-l1"><a class="reference internal" href="#">信号与系统</a>
    <ul>
                <li class="toctree-l2"><a class="reference internal" href="../../%E4%BF%A1%E5%8F%B7%E4%B8%8E%E7%B3%BB%E7%BB%9F/1.%20%E4%BF%A1%E5%8F%B7%E4%B8%8E%E7%B3%BB%E7%BB%9F/">信号与系统</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E4%BF%A1%E5%8F%B7%E4%B8%8E%E7%B3%BB%E7%BB%9F/2.%20%E7%BA%BF%E6%80%A7%E6%97%B6%E4%B8%8D%E5%8F%98%E7%B3%BB%E7%BB%9F/">线性时不变系统</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E4%BF%A1%E5%8F%B7%E4%B8%8E%E7%B3%BB%E7%BB%9F/3.%20%E5%91%A8%E6%9C%9F%E4%BF%A1%E5%8F%B7%E7%9A%84%E5%82%85%E9%87%8C%E5%8F%B6%E7%BA%A7%E6%95%B0%E8%A1%A8%E7%A4%BA/">周期信号的傅里叶级数表示</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E4%BF%A1%E5%8F%B7%E4%B8%8E%E7%B3%BB%E7%BB%9F/4.%20%E8%BF%9E%E7%BB%AD%E6%97%B6%E9%97%B4%E5%82%85%E9%87%8C%E5%8F%B6%E5%8F%98%E6%8D%A2/">连续时间傅里叶变换</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E4%BF%A1%E5%8F%B7%E4%B8%8E%E7%B3%BB%E7%BB%9F/5.%20%E7%A6%BB%E6%95%A3%E6%97%B6%E9%97%B4%E5%82%85%E9%87%8C%E5%8F%B6%E5%8F%98%E6%8D%A2/">离散时间傅里叶变换</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E4%BF%A1%E5%8F%B7%E4%B8%8E%E7%B3%BB%E7%BB%9F/6.%20%E4%BF%A1%E5%8F%B7%E4%B8%8E%E7%B3%BB%E7%BB%9F%E7%9A%84%E6%97%B6%E5%9F%9F%E5%92%8C%E9%A2%91%E5%9F%9F%E7%89%B9%E6%80%A7/">信号与系统的时域和频域特性</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E4%BF%A1%E5%8F%B7%E4%B8%8E%E7%B3%BB%E7%BB%9F/7.%20%E9%87%87%E6%A0%B7/">采样</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E4%BF%A1%E5%8F%B7%E4%B8%8E%E7%B3%BB%E7%BB%9F/9.%20%E6%8B%89%E6%99%AE%E6%8B%89%E6%96%AF%E5%8F%98%E6%8D%A2/">拉普拉斯变换</a>
                </li>
                <li class="toctree-l2"><a class="reference internal" href="../../%E4%BF%A1%E5%8F%B7%E4%B8%8E%E7%B3%BB%E7%BB%9F/10.%20z%E5%8F%98%E6%8D%A2/">z变换</a>
                </li>
    </ul>
                  </li>
              </ul>
      </div>
    </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap">
      <nav class="wy-nav-top" role="navigation" aria-label="Mobile navigation menu">
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="../..">咩咩的笔记</a>
        
      </nav>
      <div class="wy-nav-content">
        <div class="rst-content"><div role="navigation" aria-label="breadcrumbs navigation">
  <ul class="wy-breadcrumbs">
    <li><a href="../.." class="icon icon-home" aria-label="Docs"></a> &raquo;</li>
          <li>笔记 &raquo;</li>
          <li>离散数学 &raquo;</li>
      <li>命题逻辑</li>
    <li class="wy-breadcrumbs-aside">
    </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
            <div class="section" itemprop="articleBody">
              
                <h1 id="_1">离散数学第二章——命题逻辑</h1>
<h2 id="_2">基本概念</h2>
<ul>
<li>
<p><strong>命题</strong>是具有真假值的陈述句，其真假值称为<strong>真值</strong></p>
</li>
<li>
<p><strong>原子命题</strong>是不可再分解的命题，<strong>复合命题</strong>是可被分解为子命题且真值由子命题唯一确定的命题，确定的方式是将子命题用<strong>逻辑联结词</strong>联系起来</p>
</li>
<li>
<p>为了便于研究，使用符号标记原子命题，这些符号称为<strong>命题变量符号</strong>，联系逻辑也记作符号，称为<strong>逻辑运算符</strong>，由此可以将复合命题用符号表示，这串符号称为<strong>命题逻辑公式</strong></p>
</li>
</ul>
<h2 id="_3">语法</h2>
<div class="admonition note">
<p class="admonition-title">Note</p>
<p>这一小节开始，书本定义了一套公理化系统。时刻记住，很多繁琐的定义和定理其实只是因为对严谨的追求，表达的意思其实很简单。</p>
</div>
<ul>
<li>
<p>研究问题时使用的命题变量符号集合记作<strong>Var</strong>，其中的每个元素称为<strong>命题变量</strong></p>
</li>
<li>
<p>（定义2.2）命题逻辑公式由<strong>Var</strong>中定义的命题变量和逻辑运算符（<span class="arithmatex">\(\neg,\vee,\wedge,\to,\leftrightarrow\)</span>）组成</p>
</li>
<li>
<p>（定义2.2）命题逻辑公式的归纳定义：给定Var，则所有命题逻辑公式构成的集合<span class="arithmatex">\(F_{var}\)</span>为：<br />
   （1）归纳基：每个命题变量都是命题逻辑公式<br />
   （2）归纳步：若A是命题逻辑公式，则<span class="arithmatex">\((\neg A)\)</span>也是；若A、B是命题逻辑公式，则<span class="arithmatex">\((A\vee B)、(A\wedge B)、(A\to B)、(A\leftrightarrow B)\)</span>也是。</p>
</li>
<li>
<p>命题逻辑公式有且仅有6种形式<br />
   （1） 若A是命题变量，则称A是<strong>原子公式</strong><br />
   （2） 若A形式为<span class="arithmatex">\(\neg B\)</span>（非B）称为<strong>否定式</strong> <br />
   （3） 若A形式为<span class="arithmatex">\((B\wedge C)\)</span>（B与C）称为<strong>合取式</strong> <br />
   （4） 若A形式为<span class="arithmatex">\((B\vee C)\)</span>（B或C）称为<strong>析取式</strong> <br />
   （5） 若A形式为<span class="arithmatex">\((B\to C)\)</span>（B蕴含C）称为<strong>蕴含式</strong> <br />
   （6） 若A形式为<span class="arithmatex">\((B\leftrightarrow C)\)</span>（B双蕴含C）称为<strong>双蕴含式</strong>  </p>
</li>
<li>
<p>为了更清晰地展示命题逻辑公式的层次，引入<strong>抽象语法树（AST）</strong>表达法</p>
</li>
<li>
<p>（定义2.3）定义命题逻辑公式A的<strong>子公式</strong>为：<br />
   （1） 若A为命题变量，则A的子公式只有A本身<br />
   （2） 若A形式为<span class="arithmatex">\(\neg B\)</span>，则A的子公式为A和B的所有子公式<br />
   （3） 若A形式为<span class="arithmatex">\(B\oplus C\)</span>，其中<span class="arithmatex">\(\oplus\)</span>为<span class="arithmatex">\(\vee、\wedge、\to、\leftrightarrow\)</span>中的一种，则A的子公式为A和B、C的所有子公式  </p>
</li>
<li>
<p>研究语法得到两个性质：<br />
   （1） 引理2.1：命题逻辑公式的左括号数等于右括号数等于逻辑运算符数<br />
      证明过程运用到结构归纳法，基本思想是对于证明一个性质适用于任意命题逻辑公式，先证明性质对原子公式成立，再证明性质对任意公式的组合也成立，即可归纳得证<br />
   （2） 引理2.2：对于不是命题变量的命题逻辑公式，有且仅有一个运算符满足其左边公式以左括号开头且比左括号比右括号多一个，而右边公式以右括号结束且右括号比左括号多一个  </p>
<blockquote>
<p>在AST中这个逻辑运算符就是根节点</p>
</blockquote>
</li>
<li>
<p>为了简化命题逻辑公式，可以在不改变运算顺序的前提下省略括号，为此定义<strong>逻辑运算符的优先级从高到低为<span class="arithmatex">\(\neg、\wedge、\vee、\to、\leftrightarrow\)</span></strong>，且<span class="arithmatex">\(\wedge、\vee、\leftrightarrow\)</span>是从左往右结合的，而<span class="arithmatex">\(\to\)</span>是从右往左结合的</p>
</li>
</ul>
<h2 id="_4">语义</h2>
<p>这一小节主要介绍公式求值</p>
<ul>
<li>（定义2.4）为了定义公式的值，要先定义命题变量的值，为此引入真值赋值函数<span class="arithmatex">\(\sigma\)</span>，将命题变量映射到真值集{0，1}，也就是<span class="arithmatex">\(\sigma:Var\to \{0,1\}\)</span></li>
<li>拓展<span class="arithmatex">\(\sigma\)</span>的作用，使其可以对逻辑运算符进行计算（具体运算大家都会，不写了，烦死了）</li>
<li>为了计算公式的值，必须先计算子公式的值；从AST的视角看就是要先算子节点才能算父节点</li>
</ul>
<div class="admonition note">
<p class="admonition-title">Note</p>
<p>然而其实可以“剪枝”，也就是实际程序的运算符有“短路”功能，比如或运算符有一个真另一个就不用算了。书中后面有提类似方法</p>
</div>
<ul>
<li>为了全面描述公式的样貌，最好将命题变量可能出现的所有情况（<span class="arithmatex">\(2^n\)</span>种）都计算一遍，为了便于呈现，可以使用<strong>真值表</strong>表示。真值表的行按照二进制排序出所有情况，列呈现起始值（命题变量的真值）、中间量（可选，便于手算）、终值（公式的真值）</li>
</ul>
<p>逻辑运算符的真值表：</p>
<table>
<thead>
<tr>
<th>A</th>
<th>B</th>
<th><span class="arithmatex">\(\neg A\)</span>（非）</th>
<th><span class="arithmatex">\(A\wedge B\)</span>（与）</th>
<th><span class="arithmatex">\(A\vee B\)</span>（或）</th>
<th><span class="arithmatex">\(A\to B\)</span>（蕴含）</th>
<th><span class="arithmatex">\(A\leftrightarrow B\)</span>（双蕴含）</th>
</tr>
</thead>
<tbody>
<tr>
<td>0</td>
<td>0</td>
<td>1</td>
<td>0</td>
<td>0</td>
<td>1</td>
<td>1</td>
</tr>
<tr>
<td>0</td>
<td>1</td>
<td>1</td>
<td>0</td>
<td>1</td>
<td>1</td>
<td>0</td>
</tr>
<tr>
<td>1</td>
<td>0</td>
<td>0</td>
<td>0</td>
<td>1</td>
<td>0</td>
<td>0</td>
</tr>
<tr>
<td>1</td>
<td>1</td>
<td>0</td>
<td>1</td>
<td>1</td>
<td>1</td>
<td>1</td>
</tr>
</tbody>
</table>
<ul>
<li>为了简化运算，根据输出值对不同输入的反应分类公式：<br />
   （1） <strong>永真式/重言式</strong>：只输出真<br />
   （2） <strong>矛盾式/永假式</strong>：只输出假<br />
   （3） <strong>可满足的</strong>：不是矛盾式<br />
   （4） <strong>偶然式</strong>：有真有假<br />
   简化运算的方法就是，永真式和矛盾式可以直接用1和0替换</li>
<li>一些永真式：
   （1） <span class="arithmatex">\(\neg p \vee p\)</span>（排中律）
   （2） <span class="arithmatex">\(\neg (\neg p \wedge p)\)</span>
   （3） <span class="arithmatex">\(p\to p\)</span>
   （4） <span class="arithmatex">\(p\leftrightarrow p\)</span></li>
<li>（定理2,4）永真式的任意命题变量可以用其他公式<strong>替换</strong></li>
</ul>
<h2 id="_5">等值演算</h2>
<ul>
<li>（定义2.7）若对于任意的真值赋值函数<span class="arithmatex">\(\sigma:Var\to2\)</span>，命题逻辑公式A和B在<span class="arithmatex">\(\sigma\)</span>下的真值都相同，即都有<span class="arithmatex">\(\sigma(A)=\sigma(B)\)</span>，则称A和B <strong>逻辑等值</strong>，简称<strong>等值</strong>，记为<span class="arithmatex">\(A\equiv B\)</span>。通常也称<span class="arithmatex">\(A\equiv B\)</span>为<strong>逻辑等值式</strong>。注意逻辑等值式不是命题逻辑公式，不过将恒等号替换为双蕴含可以得到一条永真式。
 <strong>逻辑等值式模式</strong>（将ABC替换为公式得到它的<strong>实例</strong>）</li>
</ul>
<table>
<thead>
<tr>
<th>名称</th>
<th>逻辑等值式模式</th>
</tr>
</thead>
<tbody>
<tr>
<td>同一律</td>
<td><span class="arithmatex">\(A\wedge1\equiv A\)</span>，  <span class="arithmatex">\(A\vee0\equiv A\)</span></td>
</tr>
<tr>
<td>零律</td>
<td><span class="arithmatex">\(A\wedge0\equiv0\)</span>，<span class="arithmatex">\(A\vee1\equiv1\)</span></td>
</tr>
<tr>
<td>矛盾律</td>
<td><span class="arithmatex">\(A\wedge (\neg A)\equiv0\)</span></td>
</tr>
<tr>
<td>排中律</td>
<td><span class="arithmatex">\(A\vee(\neg A)\equiv1\)</span></td>
</tr>
<tr>
<td>双重否定律</td>
<td><span class="arithmatex">\(\neg(\neg A)\equiv A\)</span></td>
</tr>
<tr>
<td>幂等律</td>
<td><span class="arithmatex">\(A\wedge A\equiv A\)</span>，<span class="arithmatex">\(A\vee A\equiv A\)</span></td>
</tr>
<tr>
<td>交换律</td>
<td><span class="arithmatex">\(A\wedge B\equiv B\wedge A\)</span>，<span class="arithmatex">\(A\vee B\equiv B\vee A\)</span></td>
</tr>
<tr>
<td>结合律</td>
<td><span class="arithmatex">\((A\wedge(B\wedge C))\equiv((A\wedge B)\wedge C)\)</span>，<span class="arithmatex">\((A\vee(B\vee C))\equiv((A\vee B)\vee C)\)</span></td>
</tr>
<tr>
<td>分配律</td>
<td><span class="arithmatex">\((A\wedge(B\vee C))\equiv(A\wedge B)\vee(A\wedge C)\)</span>，<span class="arithmatex">\((A\vee(B\wedge C))\equiv(A\vee B)\wedge(A\vee C)\)</span></td>
</tr>
<tr>
<td>吸收律</td>
<td><span class="arithmatex">\(A\wedge(A\vee B)\equiv A\)</span>，<span class="arithmatex">\(A\vee(A\wedge B)\equiv A\)</span></td>
</tr>
<tr>
<td>德摩根律</td>
<td><span class="arithmatex">\(\neg(A\wedge B)\equiv(\neg A)\vee(\neg B)\)</span>，<span class="arithmatex">\(\neg(A\vee B)\equiv(\neg A)\wedge(\neg B)\)</span></td>
</tr>
<tr>
<td>蕴含等值式</td>
<td><span class="arithmatex">\(A\to B\equiv\neg A\vee B\)</span></td>
</tr>
<tr>
<td>双蕴含等值式</td>
<td><span class="arithmatex">\(A\leftrightarrow B\equiv(A\to B)\wedge(B\to A)\)</span></td>
</tr>
</tbody>
</table>
<ul>
<li>（定理2.6）公式A的子公式B替换成等值的公式B'，替换后的A'等值于A。</li>
<li>显然等值具有<strong>传递性</strong>，一个公式多次等值变换后仍与原公式等值，这个过程称为<strong>等值演算</strong>。</li>
</ul>
<h2 id="_6">范式</h2>
<ul>
<li>（定义2.8）<strong>析取范式</strong>是一个或多个合取式的析取（或），其中的合取式都是一个或多个文字的合取，称为<strong>简单合取式</strong>（<strong>文字</strong>指的是命题变量或命题变量的否定）；<strong>合取范式</strong>是一个或多个析取式的合取（与），其中的析取式都是一个或多个文字的析取，称为<strong>简单析取式</strong></li>
<li>每个公式都有与其逻辑等值的合取范式和析取范式，但并不唯一，而接下来定义的主合取范式和主析取范式对每条公式来说是唯一的</li>
<li>（定义2.9）若n个命题变量恰好是n个文字的合取，且每个文字对应不同的命题变量（它本身或其否定），则称该合取式为<strong>极小项</strong>。含有n个命题变量的<strong>主析取范式</strong>是零个或多个极小项的析取</li>
</ul>
<div class="admonition note">
<p class="admonition-title">Note</p>
<p>研究极小项可以发现，n个命题变量有<span class="arithmatex">\(2^n\)</span>个极小项，且每个极小项对应着真值表的一条情况。这样，只要研究原公式的真值表，并选出其中真值为真的输入对应的极小项析取起来，就得到了主析取范式</p>
</div>
<ul>
<li>（定义2.10）含n个命题变量的析取式恰好是n个文字的析取，且每个文字对应不同的命题变量，则这个析取式称为极大项。含有n个命题变量的<strong>主合取范式</strong>是零个或多个极大项的合取</li>
</ul>
<div class="admonition note">
<p class="admonition-title">Note</p>
<p>极大项就是只有一种情况真值为假，与主析取范式类似，将真值表中假的情况对应的极大项合取即可</p>
</div>
<div class="admonition note">
<p class="admonition-title">我的记忆方法</p>
<p>极大项真值表很多一所以很大；很多一说明极大项挑零，挑零的运算符是与，所以极大项对应合取范式；为了有很多一，要用或来连接命题变量，所以是简单析取式。极小项同理</p>
</div>
<ul>
<li>除了用真值表，也可以用等值演算来求。如果遇到缺少命题变量的情况，可以用矛盾律或排中律无中生有。另外，真值表、主合取范式和主析取范式可以互推，主合取范式和主析取范式互推时文字记得取反。</li>
</ul>
<div class="admonition note">
<p class="admonition-title">Note</p>
<p>实践证明直接等值演算一般比真值表难做。但如果公式可以化成范式，可以用待定编码的形式快速得到极大项或极小项，参见P69的解法。</p>
</div>
<h2 id="_7">推理理论</h2>
<ul>
<li>（定义2.11）<strong>推理</strong><span class="arithmatex">\(A_1,A_2...,A_n\implies B\)</span><strong>有效</strong>是指<span class="arithmatex">\(A_1\wedge A_2\wedge...\wedge A_n\to B\)</span>是永真式</li>
<li>推理为真不代表结论为真，因为条件不一定全为真</li>
<li>自然推理系统：对于任意逻辑公式A,B，以下推理有效</li>
</ul>
<table>
<thead>
<tr>
<th>名称</th>
<th>规则</th>
</tr>
</thead>
<tbody>
<tr>
<td>假言推理（分离规律）</td>
<td><span class="arithmatex">\(A\to B,A\implies B\)</span></td>
</tr>
<tr>
<td>假言易位（拒取式）</td>
<td><span class="arithmatex">\(A\to B,\neg B\implies \neg A\)</span></td>
</tr>
<tr>
<td>合取</td>
<td><span class="arithmatex">\(A,B\implies A\wedge B\)</span></td>
</tr>
<tr>
<td>化简</td>
<td><span class="arithmatex">\(A\wedge B\implies A\)</span></td>
</tr>
<tr>
<td>附加</td>
<td><span class="arithmatex">\(A\implies A\vee B\)</span></td>
</tr>
<tr>
<td>析取三段论</td>
<td><span class="arithmatex">\(\neg A,A\vee B\implies B\)</span></td>
</tr>
<tr>
<td>等值置换</td>
<td><span class="arithmatex">\(若A\equiv B，则A\implies B,B\implies A\)</span></td>
</tr>
</tbody>
</table>
<p>假言推理和假言易位可利用蕴含式前提；</p>
<ul>
<li>（定义2.13）<strong>论证</strong>或<strong>证明</strong>是打竖写每行一个公式的公式序列，<em>每一行都是推理前提</em>或者<em>用前面行可以推理出的公式</em>，最后以结论为结尾</li>
<li>论证中每行开头标注序号；分析过程中待定的序号写问号，稍后在完整证明中补全；每行末尾注释公式来源（应用等值置换规则则要写出对应的逻辑等值模式，只能用双蕴含等值式、双重否定律、交换律，且不对公式的子公式应用等值置换）  </li>
<li>（定理2.7）如果推理存在<strong>论证</strong>，它就是有效的  </li>
<li>只能用具体的公式替换规则中的字母，不能替换规则中的子公式</li>
</ul>
<h3 id="_8">派生规则</h3>
<ul>
<li><strong>双蕴含推理</strong>规则：<span class="arithmatex">\(A\leftrightarrow B \implies A \to B\)</span>，<span class="arithmatex">\(A\leftrightarrow B \implies B \to A\)</span></li>
<li>（定理2.8）<strong>附加前提法</strong> ：对于任意公式<span class="arithmatex">\(A_1,A_2,\cdots,An,B,C\)</span>，推理<span class="arithmatex">\(A_1,A_2,\cdots,A_n\implies B\to C\)</span>是有效的，当且仅当推理<span class="arithmatex">\(A_1,A_2,\cdots,A_n,B\implies C\)</span>是有效的。（需要注意的是从引入附加前提到消除附加前提的公式可能依赖于附加前提，所以在论证结束之前要消除附加前提）</li>
<li><strong>假言三段论</strong>：<span class="arithmatex">\(A\to B,B\to C\implies A\to C\)</span></li>
<li>（定理2.9）<strong>反证法</strong>：对任意公式<span class="arithmatex">\(A_1,A_2,\cdots,A_n,B\)</span>，推理<span class="arithmatex">\(A_1,A_2,\cdots,A_n\implies \neg B\)</span>是有效的当且仅当存在公式C使得推理<span class="arithmatex">\(A_1,A_2,\cdots,A_n,B\implies C\wedge \neg C\)</span>是有效的 </li>
</ul>
<h2 id="_9">应用</h2>
<p>基本思路都是先抽象出原子命题、逻辑符号，将问题转化为命题逻辑公式或推理，再进行等值演算、论证等运算。</p>
<h3 id="_10">自然语言命题的符号化</h3>
<ul>
<li><strong>联言判断</strong>：自然语言中的“与”逻辑</li>
<li><strong>选言判断</strong>：类似于“或”逻辑，但现实中的或分相容和不相容（即是否可以同时成立），相容就是“或”逻辑，不相容就是“异或”逻辑（为避免歧义，模糊说法算相容）</li>
<li><strong>假言判断</strong>：表达充分条件和必要条件，对应“蕴含”逻辑（有时可能包含“双蕴含”逻辑，为避免歧义，模糊说法算蕴含）</li>
</ul>
<h3 id="_11">普通逻辑问题的符号化</h3>
<p>逻辑问题有三类：</p>
<ul>
<li>给定条件，寻找满足条件的情况<br />
   这种问题的条件可以转换为命题公式。问题中的条件组合称为<strong>规范</strong>，如果命题公式可满足（即可以为真）则称规则是<strong>一致的</strong>。</li>
<li>给定前提，推出结论<br />
   这种问题可以转化为逻辑推理问题。</li>
<li>给定前提，探求可以推理出的结论<br />
   可以用逻辑推理，也可以转化为问题一</li>
</ul>
<h3 id="_12">算法性质的逻辑分析</h3>
              
            </div>
          </div><footer>
    <div class="rst-footer-buttons" role="navigation" aria-label="Footer Navigation">
        <a href="../../%E6%95%B0%E5%AD%97%E7%94%B5%E8%B7%AF/11.%20%E6%A8%A1%E6%95%B0%E8%BD%AC%E6%8D%A2/" class="btn btn-neutral float-left" title="模数转换"><span class="icon icon-circle-arrow-left"></span> Previous</a>
        <a href="../3-%E4%B8%80%E9%98%B6%E9%80%BB%E8%BE%91/" class="btn btn-neutral float-right" title="一阶逻辑">Next <span class="icon icon-circle-arrow-right"></span></a>
    </div>

  <hr/>

  <div role="contentinfo">
    <!-- Copyright etc -->
  </div>

  Built with <a href="https://www.mkdocs.org/">MkDocs</a> using a <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a> provided by <a href="https://readthedocs.org">Read the Docs</a>.
</footer>
          
        </div>
      </div>

    </section>

  </div>

  <div class="rst-versions" role="note" aria-label="Versions">
  <span class="rst-current-version" data-toggle="rst-current-version">
    
    
      <span><a href="../../%E6%95%B0%E5%AD%97%E7%94%B5%E8%B7%AF/11.%20%E6%A8%A1%E6%95%B0%E8%BD%AC%E6%8D%A2/" style="color: #fcfcfc">&laquo; Previous</a></span>
    
    
      <span><a href="../3-%E4%B8%80%E9%98%B6%E9%80%BB%E8%BE%91/" style="color: #fcfcfc">Next &raquo;</a></span>
    
  </span>
</div>
    <script>var base_url = '../..';</script>
    <script src="../../js/theme_extra.js" defer></script>
    <script src="../../js/theme.js" defer></script>
      <script src="../../javascripts/mathjax.js" defer></script>
      <script src="https://fastly.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js" defer></script>
      <script src="../../search/main.js" defer></script>
    <script defer>
        window.onload = function () {
            SphinxRtdTheme.Navigation.enable(true);
        };
    </script>

</body>
</html>
